$\forall$$T$:Type.
\\[0ex]$T$ $\subseteq\rho$ $\mathbb{Z}$ $\Rightarrow$ ($\forall$${\it as}$:$T$ List. sorted(${\it as}$) \& no\_repeats($T$;${\it as}$) $\Leftrightarrow$ ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it as}$$\parallel$}}$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$i$}}$. ${\it as}$[$j$]$<$${\it as}$[$i$]))